\begin{tabbing}
discrete{-}pre{-}p(${\it es}$;$i$;${\it ds}$;$a$;$p$;$P$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$x$:Id. subtype\_rel(es{-}vartype(${\it es}$; $i$; $x$); fpf{-}cap(${\it ds}$; id{-}deq; $x$; top)))\+
\\[0ex]c$\wedge$ \=(alle{-}at(\=${\it es}$;\+\+
\\[0ex]$i$;
\\[0ex]$e$.((es{-}kind(${\it es}$; $e$) = locl($a$) $\in$ Knd)
\\[0ex]$\Rightarrow$ \=(subtype\_rel(es{-}valtype(${\it es}$; $e$); p{-}outcome($p$))\+
\\[0ex]c$\wedge$ ($\uparrow$($P$(es{-}state{-}when(${\it es}$; $e$)))))))
\-\-\\[0ex]$\wedge$ \=(es{-}dds(${\it es}$;$i$;${\it ds}$)\+
\\[0ex]$\Rightarrow$ \=(alle{-}at(\=${\it es}$;\+\+
\\[0ex]$i$;
\\[0ex]$e$.existse{-}ge(\=${\it es}$;\+
\\[0ex]$e$;
\\[0ex]${\it e'}$.((es{-}kind(${\it es}$; ${\it e'}$) = locl($a$) $\in$ Knd)
\\[0ex]$\vee$ ($\neg$($\uparrow$($P$(es{-}state{-}after(${\it es}$; ${\it e'}$))))))))
\-\-\\[0ex]$\wedge$ \=(($\uparrow$($P$(es{-}init{-}state(${\it es}$; $i$))))\+
\\[0ex]$\Rightarrow$ ($\exists$$e$:es{-}E(${\it es}$). (es{-}loc(${\it es}$; $e$) = $i$ $\in$ Id))))))
\-\-\-\-\-
\end{tabbing}